/-
Copyright (c) 2025 Antoine Chambert-Loir. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Antoine Chambert-Loir
-/

import Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
import Mathlib.GroupTheory.SpecificGroups.KleinFour
import Mathlib.GroupTheory.Sylow

/-! # The Klein Four subgroup of an alternating group on 4 letters

Let `α` be a finite type such that `Nat.card α = 4`.

* `alternatingGroup.kleinFour` : the subgroup of `alternatingGroup α` generated by permutations of
  cycle type (2, 2).

## Main results

* `alternatingGroup.kleinFour_isKleinFour`: `alternatingGroup.kleinFour α` satisfies `IsKleinFour`.
  (When `4 < Nat.card α`, it is equal to `⊤`, when `Nat.card α < 4`, it is trivial.)

* `alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four`:
  All `2`-sylow subgroups of `alternatingGroup α` are equal to `kleinFour α`.

* `alternatingGroup.characteristic_kleinFour`:
  the subgroup `alternatingGroup.kleinFour α` is characteristic.

* `alternatingGroup.kleinFour_eq_commutator`:
  the subgroup `alternatingGroup.kleinFour α` is the commutator subgroup of `alternatingGroup α`.
  (When `4 < Nat.card α`, the commutator subgroup of `alternatingGroup α` is equal to `⊤`;
  when `Nat.card α < 3`, it is trivial.)

## Remark on implementation

We start from `alternatingGroup.kleinFour α` as given by its definition.
We first prove that it is equal to any 2-sylow subgroup:
the elements of such a sylow subgroup `S` have order a power of 2,
and this implies that their cycle type is () or (2,2).
Since there are exactly 4 elements of that cycle type,
we conclude that `alternatingGroup.kleinFour α = S`.
Since all 2-sylow subgroups are conjugate, we conclude
that there is only one 2-sylow subgroup and that it is normal,
and then characteristic.

## TODO :

Prove `alternatingGroup.kleinFour α = commutator (alternatingGroup α)`
without any assumption on `Nat.card α`.

-/

namespace alternatingGroup

open Equiv.Perm Equiv

variable {α : Type*} [DecidableEq α] [Fintype α]

variable (α) in
/-- The subgroup of `alternatingGroup α` generated by permutations of cycle type (2, 2).

When `Nat.card α = 4`, it will effectively be of Klein Four type. -/
def kleinFour : Subgroup (alternatingGroup α) :=
  Subgroup.closure {g : alternatingGroup α | (g : Equiv.Perm α).cycleType = {2, 2}}

theorem mem_kleinFour_of_order_two_pow (hα4 : Nat.card α = 4) {g : Perm α}
    (hg0 : g ∈ alternatingGroup α) {n : ℕ} (hg : orderOf g ∣ 2 ^ n) :
    g.cycleType = { } ∨ g.cycleType = {2, 2} := by
  rw [mem_alternatingGroup, sign_of_cycleType] at hg0
  have h1 : g.cycleType.sum ≤ 4 := by
    rw [sum_cycleType, ← hα4, Nat.card_eq_fintype_card]
    exact g.support.card_le_univ
  have h2 : ∀ k ∈ g.cycleType, k = 2 := by
    intro k hk
    have hk4 := (Multiset.le_sum_of_mem hk).trans h1
    have hk1 := one_lt_of_mem_cycleType hk
    interval_cases k
    · rfl
    · rw [← lcm_cycleType, Multiset.lcm_dvd] at hg
      exact Nat.prime_eq_prime_of_dvd_pow Nat.prime_three Nat.prime_two (hg 3 hk)
    · contrapose! hg0
      obtain ⟨t, ht⟩ := Multiset.exists_cons_of_mem hk
      rw [ht, Multiset.sum_cons, add_le_iff_nonpos_right, le_zero_iff,
        Multiset.sum_eq_zero_iff, ← Multiset.eq_replicate_card] at h1
      have h : 0 ∉ g.cycleType := Nat.not_succ_lt_self ∘ one_lt_of_mem_cycleType
      replace h : t = 0 := by simpa [h1 ▸ ht, Multiset.mem_replicate] using h
      simp [ht, h, Units.ext_iff]
  rw [← Multiset.eq_replicate_card] at h2
  rw [h2, Multiset.sum_replicate, smul_eq_mul, ← Nat.le_div_iff_mul_le two_pos] at h1
  interval_cases g.cycleType.card <;> simp [h2, Units.ext_iff] at hg0 ⊢

theorem card_of_card_eq_four (hα4 : Nat.card α = 4) :
    Nat.card (alternatingGroup α) = 12 := by
  have : Nontrivial α := by
    rw [← Finite.one_lt_card_iff_nontrivial, hα4]
    simp
  rw [nat_card_alternatingGroup, hα4]
  decide

theorem card_two_sylow_of_card_eq_four (hα4 : Nat.card α = 4) (S : Sylow 2 (alternatingGroup α)) :
    Nat.card S = 4 := by
  rw [Sylow.card_eq_multiplicity, card_of_card_eq_four hα4]
  have : 12 = 2 ^ 2 * 3 := by simp
  rw [this, Nat.factorization_mul_apply_of_coprime (by decide), Nat.factorization_pow,
    Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, Nat.prime_two.factorization_self,
    Nat.factorization_eq_zero_of_not_dvd (by decide)]
  simp

theorem coe_two_sylow_of_card_eq_four
    (hα4 : Nat.card α = 4) (S : Sylow 2 (alternatingGroup α)) :
    (S : Set (alternatingGroup α)) =
      {1} ∪ {g : alternatingGroup α | (g : Perm α).cycleType = {2, 2}} := by
  classical
  refine Set.eq_of_subset_of_card_le (fun k hk ↦ ?_) ?_
  · -- inclusion S ⊆ {1} ∪ {g |  cycleType g = { 2, 2 }}
    obtain ⟨n, hn⟩ := (IsPGroup.iff_orderOf.mp S.isPGroup') ⟨k, hk⟩
    replace hn : (orderOf (k : Perm α)) = 2 ^ n := by simpa using hn
    convert mem_kleinFour_of_order_two_pow hα4 k.2 hn.dvd
    simp
  · -- card (kleinFour α) ≤ card S
    simp_rw [← Nat.card_eq_fintype_card]
    refine (card_two_sylow_of_card_eq_four hα4 S).symm.trans_ge ?_
    rw [Nat.card_eq_card_toFinset, Set.toFinset_union, Set.toFinset_singleton, Set.toFinset_setOf]
    apply (Finset.card_union_le _ _).trans
    rw [Finset.card_singleton, AlternatingGroup.card_of_cycleType, ← Nat.card_eq_fintype_card, hα4]
    decide

theorem two_sylow_eq_kleinFour_of_card_eq_four
    (hα4 : Nat.card α = 4) (S : Sylow 2 (alternatingGroup α)) :
    S = kleinFour α := by
  rw [kleinFour, ← Subgroup.closure_insert_one,
    ← Set.singleton_union, ← coe_two_sylow_of_card_eq_four hα4]
  exact S.closure_eq.symm

theorem subsingleton_two_sylow (hα4 : Nat.card α = 4) :
    Subsingleton (Sylow 2 (alternatingGroup α)) where
  allEq S T := by
    rw [Sylow.ext_iff]
    simp [two_sylow_eq_kleinFour_of_card_eq_four hα4]

theorem characteristic_kleinFour (hα4 : Nat.card α = 4) :
    (kleinFour α).Characteristic := by
  obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
  have _ := subsingleton_two_sylow hα4
  rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S]
  exact Sylow.characteristic_of_subsingleton _

theorem normal_kleinFour (hα4 : Nat.card α = 4) :
    (kleinFour α).Normal := by
  have _ := characteristic_kleinFour hα4
  apply Subgroup.normal_of_characteristic

theorem kleinFour_card_of_card_eq_four (hα4 : Nat.card α = 4) :
    Nat.card (kleinFour α) = 4 := by
  obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
  rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S, card_two_sylow_of_card_eq_four hα4 S]

theorem coe_kleinFour_of_card_eq_four (hα4 : Nat.card α = 4) :
    (kleinFour α : Set (alternatingGroup α)) =
      {1} ∪ {g : alternatingGroup α | (g : Equiv.Perm α).cycleType = {2, 2}} := by
  obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
  rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S]
  exact coe_two_sylow_of_card_eq_four hα4 S

theorem exponent_kleinFour_of_card_eq_four (hα4 : Nat.card α = 4) :
    Monoid.exponent (kleinFour α) = 2 := by
  have : Monoid.exponent (kleinFour α) ∣ 2 := by
    rw [Monoid.exponent_dvd]
    rintro ⟨⟨g, hg⟩, hg'⟩
    simp only [Subgroup.orderOf_mk, orderOf_dvd_iff_pow_eq_one]
    rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4] at hg'
    rcases hg' with hg' | hg'
    · convert one_pow _
      simpa only [Set.mem_singleton_iff, Subgroup.mk_eq_one] using hg'
    · convert pow_orderOf_eq_one g
      rw [← Equiv.Perm.lcm_cycleType, hg']
      simp
  rw [Nat.dvd_prime Nat.prime_two] at this
  apply Or.resolve_left this
  rw [Monoid.exp_eq_one_iff, ← Finite.card_le_one_iff_subsingleton,
    kleinFour_card_of_card_eq_four hα4]
  decide

theorem kleinFour_isKleinFour (hα4 : Nat.card α = 4) :
    IsKleinFour (kleinFour α) where
  card_four := kleinFour_card_of_card_eq_four hα4
  exponent_two := exponent_kleinFour_of_card_eq_four hα4

theorem kleinFour_eq_commutator (hα4 : Nat.card α = 4) :
    kleinFour α = commutator (alternatingGroup α) := by
  have _ : (kleinFour α).Normal := normal_kleinFour hα4
  have : Nat.card (alternatingGroup α ⧸ kleinFour α) = 3 := by
    rw [← Nat.mul_left_inj (a := Nat.card (kleinFour α))]
    · rw [← Subgroup.card_eq_card_quotient_mul_card_subgroup]
      rw [card_of_card_eq_four hα4, kleinFour_card_of_card_eq_four hα4]
    rw [kleinFour_card_of_card_eq_four hα4]; simp
  have comm_le : commutator (alternatingGroup α) ≤ kleinFour α := by
    rw [← Subgroup.Normal.quotient_commutative_iff_commutator_le]
    exact (isCyclic_of_prime_card this).commutative
  have comm_ne_bot : commutator (alternatingGroup α) ≠ ⊥ := by
    rw [ne_eq, commutator_eq_bot_iff_center_eq_top,
      center_eq_bot (le_of_eq hα4.symm)]
    apply @bot_ne_top _ _ _ ?_
    rw [Subgroup.nontrivial_iff, ← Finite.one_lt_card_iff_nontrivial,
      card_of_card_eq_four hα4]
    simp
  obtain ⟨k, hk, hk'⟩ := Or.resolve_left (Subgroup.bot_or_exists_ne_one _) comm_ne_bot
  suffices hk22 : (k : Equiv.Perm α).cycleType = {2, 2} by
    refine le_antisymm ?_ comm_le
    intro g hg
    rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4,
      Set.mem_union, Set.mem_singleton_iff, Set.mem_setOf_eq] at hg
    rcases hg with ⟨rfl⟩ | hg
    · exact Subgroup.one_mem _
    · rw [← hg, ← Equiv.Perm.isConj_iff_cycleType_eq, isConj_iff] at hk22
      obtain ⟨c, hc⟩ := hk22
      rw [← MulAut.conjNormal_apply, Subtype.coe_inj] at hc
      simp only [commutator, ← hc]
      let fc : MulAut (alternatingGroup α) := MulAut.conjNormal c
      suffices (⊤ : Subgroup (alternatingGroup α)) =
        Subgroup.map fc.toMonoidHom (⊤ : Subgroup (alternatingGroup α)) by
        rw [this, ← Subgroup.map_commutator]
        refine Subgroup.mem_map_of_mem _ hk
      apply symm
      rw [← MonoidHom.range_eq_map]
      rw [MonoidHom.range_eq_top]
      exact MulEquiv.surjective _
  have hk2 := comm_le hk
  rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4,
    Set.mem_union, Set.mem_singleton_iff, Set.mem_setOf_eq] at hk2
  exact hk2.resolve_left hk'

end alternatingGroup
